Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B

摘要

Standards play the key role in safety-critical systems. Errors in standardscould mislead system developer's understanding and introduce bugs into systemimplementations. In this paper, we present an Event-B formalization andverification for the ARINC 653 standard, which provides a standardizedinterface between safety-critical real-time operating systems and applicationsoftware, as well as a set of functionalities aimed to improve the safety andcertification process of such safety-critical systems. The formalization is acomplete model of ARINC 653, and provides a necessary foundation for the formaldevelopment and verification of ARINC 653 compliant operating systems andapplications. Six hidden errors were discovered from the verification using theEvent-B formal reasoning approach.